SherbyNet - /page/wikibook/entry.mu

Micron Document

`:top

La `!machine SECD`! est une `F33f`_`[machine virtuelle`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Machine_virtuelle]`_`f (dite encore `F33f`_`[machine abstraite`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Machine_abstraite]`_`f) qui a été conçue pour servir de cible`:cite-ref-1[`F5bf`_`[1`#cite-note-1]`_`f] à la `F33f`_`[compilation`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Compilation_(informatique)]`_`f des premiers langages de programmation et a eu une grande influence sur les origines de l'informatique et des langages de programmation, y compris la `F33f`_`[machine virtuelle Java`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Machine_virtuelle_Java]`_`f. Son `F33f`_`[acronyme`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Acronymie]`_`f SECD provient des quatre constituants de son état`:cite-ref-2[`F5bf`_`[2`#cite-note-2]`_`f] à savoir la `*pile`* (`!s`!tack en anglais), l'`!e`!nvironnement, le `!c`!ontrôle, le `!d`!épôt (`!d`!ump en anglais).

Cette machine, due à `F33f`_`[Peter J. Landin`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Peter_J._Landin]`_`f, a été la première description formelle de l'évaluation du `F33f`_`[lambda-calcul`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Lambda-calcul]`_`f et fut élaborée en 1963 en association avec son projet de langage de programmation `F33f`_`[ISWIM`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=ISWIM]`_`f. Comme la description originelle de Landin laissait beaucoup de détails dans l'ombre, la présentation de la SECD qui est la plus communément acceptée est celle que Peter Henderson a faite en 1980 dans le cadre de son compilateur `F33f`_`[Lisp`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Lisp]`_`f `*Lispkit`*. Depuis, elle a été utilisée comme cible de plusieurs compilateurs et en particulier comme base d'une implantation matérielle réalisée par des chercheurs de l'université de Calgary`:cite-ref-3[`F5bf`_`[3`#cite-note-3]`_`f].

>>Contents

• `F0af`_`[Description informelle`#description-informelle]`_`f

• `F0af`_`[Transitions`#transitions]`_`f

• `F0af`_`[Début et fin`#d-but-et-fin]`_`f

• `F0af`_`[Aspect historique`#aspect-historique]`_`f

• `F0af`_`[Notes et références`#notes-et-r-f-rences]`_`f

• `F0af`_`[Bibliographie`#bibliographie]`_`f

• `F0af`_`[Voir aussi`#voir-aussi]`_`f

-─

>>Description informelle

La machine SECD est une machine à base de piles et de valeurs, qui implante l'`*`F33f`_`[appel par valeur`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Stratégie_d'évaluation_(informatique)]`_`f`* pour le lambda-calcul. En lambda-calcul, une `*valeur`* est soit une variable, soit une `F33f`_`[abstraction`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Lambda-calcul]`_`f. Évaluer en `*appel par valeur`* signifie que l'on évalue une expression `*(λ x. A) B`*, en évaluant `*B`* puis `*λ x. A`*. Dit autrement, on évalue l'appel d'une fonction appliquée à des paramètres en évaluant d'abord les paramètres, puis le corps de la fonction. Dans la machine SECD, la pile `!S`! et l'environnement `!E`! ne stockent que des valeurs, tandis que `!D`! sert à évaluer le reste, c'est-à-dire les applications. Un `*état`* de la machine est un quadruplet (`!S`!, `!E`!, `!C`!, `!D`!).

>>>Transitions

Avant de commencer, l'expression à évaluer est traduite en `F33f`_`[notation polonaise inverse`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Notation_polonaise_inverse]`_`f avec comme seul opérateur `!ap`! (c'est-à-dire l'opérateur d'application), puis installée dans la partie `!C`! de l'état (le contrôle), tandis que `!E`!, `!S`! et `!D`! sont vides. Par exemple l'expression `*x (y z)`* produit l'expression `*z`* : `*y`* : `!ap`! : `*x`* : `!ap`! qui est la `F33f`_`[liste`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Liste_(informatique)]`_`f `*[z, y, `!ap`!, x, `!ap`!]`*. La machine passe d'un état à un autre comme suit.

• Si le premier élément de la liste `!C`! est une valeur, elle est mise sur la pile. Plus précisément,

• si cette tête de liste est une variable, l'expression mise sur la pile `!S`! est la valeur associée à cette variable dans l'environnement `!E`!,

• si cette tête de liste est une `F33f`_`[abstraction`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Lambda-calcul]`_`f, une `F33f`_`[clôture`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Fermeture_(informatique)]`_`f est alors créée avec l'environnement `!E`! et mise sur la pile `!S`!.

• Si le premier élément de la liste `!C`! est un opérateur `!ap`!, le sommet de la pile est`:cite-ref-4[`F5bf`_`[4`#cite-note-4]`_`f] une valeur `*v`* suivie d'une abstraction `*λ x. c`*. Le contenu de `!S`!, `!E`! et `!C`! est mis sur `!D`! (qui fonctionne comme une pile de triplets) tandis que `!S`! est réinitialisé à vide (noté □), `!C`! est réinitialisé à `*c`* et `!E`! est réinitialisé à `!E`! enrichi de la liaison de `*x`* à la valeur `*v`* ; puis l'évaluation continue à partir de ce nouvel état.

• Une évaluation incomplète est terminée quand la liste `!C`! du contrôle est vide, auquel cas un résultat `*v`* se trouve sur le sommet de la pile `!S`!. Mais, à ce stade, si le dépôt `!D`! n'est pas vide, le calcul n'est pas terminé. Les trois constituants `!S`!, `!E`!, `!C`! sont alors dépilés du dépôt `!D`! et rétablis dans l'état courant, puis on ajoute `*v`* sur le sommet de la nouvelle pile, initiant un nouveau calcul.

• Quand `!C`! et `!D`! sont vides le calcul est complètement terminé et le résultat final se trouve dans la pile `!S`!.

Écrit sous forme de règles cela donne:

`*(S, E, x:C, D) ➝ (E(x) : S, E, C, D)`*

`*(S, E, (λ x. C') : C, D) ➝ (<(λ x. C'), E> : S, E, C, D)`*

`*(v : <(λ x. C'), E'> : S, E, `!ap`! : C, D) ➝ (□, E'+(x ↦ v), C', (S, E, C) : D)`*

`*(v : S, E, □, (S', E', C') : D) ➝ (v : S', E', C', D)`*

`*E(x)`* est la valeur associée à `*x`* dans l'environnement `*E`* et `*E'+(x ↦ v)`* est l'environnement `*E'`* enrichi de la liaison de `*v`* à `*x`*.

>>>Début et fin

L' `*état initial`* est `*(□, □ , `!C`!, □)`* et l' `*état final`* est `*([v], `!E`!, □, □)`*

>>Aspect historique

La machine SECD doit être replacée dans un contexte historique (1963) où les langages de `F33f`_`[programmation fonctionnelle`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Programmation_fonctionnelle]`_`f naissent, où la `F33f`_`[récursivité`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Récursivité]`_`f en informatique est embryonnaire, où la notion de `F33f`_`[pile`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Pile_(informatique)]`_`f est à peine dégagée`:cite-ref-5[`F5bf`_`[5`#cite-note-5]`_`f] tandis qu'émergent les méthodes d'évaluation (appel par nom et appel par valeur). Si on se souvient qu'elle est la première machine abstraite d'implantation d'un langage de programmation jamais inventée, on comprend que Peter J. Landin fasse figure de visionnaire et que la SECD ait marqué une étape fondamentale dans la compréhension de la récursivité qui commence à apparaître dans les langages de programmation comme `F33f`_`[Algol 60`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Algol_60]`_`f.

>>Notes et références

`:cite-note-1`!1.`! `F0af`_`[↑`#cite-ref-1]`_`f En `F33f`_`[compilation`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Compilation_(informatique)]`_`f le `*langage cible`* est le langage dans lequel le compilateur traduit les programmes du langage source. Ici on ne peut pas parler de langage cible puisqu'il s'agit d'une machine abstraite vers laquelle on traduit. On parle donc seulement de cible.

`:cite-note-2`!2.`! `F0af`_`[↑`#cite-ref-2]`_`f L'`*état`* d'une machine virtuelle est une structure de donnée qui est transformée par les transitions de la machine.

`:cite-note-3`!3.`! `F0af`_`[↑`#cite-ref-3]`_`f Un article sur la conception SECD: DESIGN ISSUES est disponible.

`:cite-note-4`!4.`! `F0af`_`[↑`#cite-ref-4]`_`f C'est toujours ainsi dans un calcul qui se déroule correctement !

`:cite-note-5`!5.`! `F0af`_`[↑`#cite-ref-5]`_`f `F33f`_`[Claude Pair`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Claude_Pair]`_`f n'a soumis sa thèse `*Étude de la notion de pile : application à l'analyse syntaxique`* qu'en 1966.

>>Bibliographie

• `F33f`_`[Danvy, Olivier`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Olivier_Danvy]`_`f. `*A Rational Deconstruction of Landin's SECD Machine`*. BRICS research report RS-04-30, 2004. ISSN 0909-0878

• Field, Anthony J. Field and Peter G. Harrison. 1988 `*Functional Programming`*. `F33f`_`[Addison-Wesley`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Addison-Wesley]`_`f. (`F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=International_Standard_Book_Number]`_`f 0-201-19249-7)

• Graham, Brian T. 1992 "The SECD Microprocessor: A Verification Case Study". Springer. (`F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=International_Standard_Book_Number]`_`f 0-7923-9245-0)

• Henderson, Peter. 1980 `*Functional Programming: Application and Implementation`*. `F33f`_`[Prentice Hall`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Prentice_Hall]`_`f. (`F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=International_Standard_Book_Number]`_`f 0-13-331579-7)

• Kogge, Peter M. `*The Architecture of Symbolic Computers`*. (`F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=International_Standard_Book_Number]`_`f 0-07-035596-7)

• `:landin1964`a`:peter-j-landin1964`a`F33f`_`[Peter J. Landin`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Peter_J._Landin]`_`f, « The Mechanical Evaluation of Expressions », `*`F33f`_`[Comput. J.`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=The_Computer_Journal]`_`f`*, vol. 6, no 4,‎ janvier 1964, p. 308–320 (`F33f`_`[DOI`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Digital_Object_Identifier]`_`f 10.1093/comjnl/6.4.308)

• `:landin1966`a`:peter-j-landin1966`a`F33f`_`[Peter J. Landin`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Peter_J._Landin]`_`f, « The next 700 programming languages », `*`F33f`_`[Comm. ACM`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Communications_of_the_ACM]`_`f`*, vol. 9, no 3,‎ mars 1966, p. 157–166 (`F33f`_`[DOI`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Digital_Object_Identifier]`_`f 10.1145/365230.365257, lire en ligne)

>>Voir aussi

• `F33f`_`[Sémantique des langages de programmation`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Sémantique_des_langages_de_programmation]`_`f

• `F33f`_`[Sémantique opérationnelle`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Sémantique_opérationnelle]`_`f

• `F33f`_`[Machine de Krivine`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Machine_de_Krivine]`_`f

• `F33f`_`[Machine virtuelle Java`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Machine_virtuelle_Java]`_`f

• `F33f`_`[Système de transition d'états`:/page/wikibook/entry.mu`zim=wikipedia_fr_all_nopic_2025-10.zim|entry_path=Système_de_transition_d'états]`_`f

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « SECD machine » (voir la liste des auteurs).

• Portail de la logique

• Portail de l'informatique théorique

• Portail de l’informatique

• Portail de la programmation informatique

`c`F0af`_`[↑ Back to top`#top]`_`f`a